Nuprl Lemma : fpf-single_wf2
11,40
postcript
pdf
A
,
B
:Type,
x
:
A
,
v
:
B
,
eqa
:EqDecider(
A
).
x
:
v
a
:
A
fp
x
:
B
(
a
)?Top
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
x
.
t
(
x
)
,
f
(
x
)?
z
,
x
:
v
,
x
dom(
f
)
,
f
(
x
)
,
deq-member(
eq
;
x
;
L
)
,
t
.1
,
t
.2
,
reduce(
f
;
k
;
as
)
,
Y
,
if
b
then
t
else
f
fi
,
p
q
,
tt
,
x
(
s
)
Lemmas
fpf-single
wf
,
deq
wf
,
ifthenelse
wf
,
bor
wf
,
eqof
wf
,
bfalse
wf
,
top
wf
,
eqof
eq
btrue
origin
A, B:Type, x:A, v:B, eqa:EqDecider(A). x : v 
a:A fp
x : B(a)?Top A, B:Type, x:A, v:B, eqa:EqDecider(A). x : v a:A fp x : B(a)?Top x:A. B(x) T
x. t(x) dom(f)
q